A:MsgA. ma-frame-compatible(;A) 

latex

Definitions

IdLnk, t  T, Knd, x:AB(x), Void, Type, x.A(x), x:A. B(x), x. t(x), 2of(t), rcv(l,tg), KindDeq, f(x)?z, type List, Top, 1of(t), x:AB(x), IdDeq, Id, a:A fp B(a), IdLnkDeq, product-deq(A;B;a;b), x  dom(f), b, False, P  Q, f(x), map(f;as), (x  l), Prop, locl(a), P & Q, xdom(f). v=f(x)   P(x;v), z != f(x)  P(a;z), Valtype(da;k), State(ds), M.ds(x), M.dout(l,tg), M.da(a), M.state, (s1  s2 mod x), M.rframe(A.sends tfL of k on l), mk-ma, M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), MsgA, ma-frame-compat(A;B), , ma-frame-compatible(A;B)

Lemmas

msga wf, locl wf, l member wf, map wf, fpf-ap wf, false wf, assert wf, fpf-dom wf, product-deq wf, idlnk-deq wf, fpf-trivial-subtype-top, Id wf, id-deq wf, pi1 wf, top wf, fpf-cap wf, Kind-deq wf, rcv wf, pi2 wf, Knd wf, IdLnk wf